home *** CD-ROM | disk | FTP | other *** search
/ Aminet 30 / Aminet 30 (1999)(Schatztruhe)[!][Apr 1999].iso / Aminet / dev / lang / SmallEiffel.lha / SmallEiffel / lib_se / class_invariant.e < prev    next >
Text File  |  1998-12-22  |  5KB  |  188 lines
  1. --          This file is part of SmallEiffel The GNU Eiffel Compiler.
  2. --          Copyright (C) 1994-98 LORIA - UHP - CRIN - INRIA - FRANCE
  3. --            Dominique COLNET and Suzanne COLLIN - colnet@loria.fr 
  4. --                       http://www.loria.fr/SmallEiffel
  5. -- SmallEiffel is  free  software;  you can  redistribute it and/or modify it 
  6. -- under the terms of the GNU General Public License as published by the Free
  7. -- Software  Foundation;  either  version  2, or (at your option)  any  later 
  8. -- version. SmallEiffel is distributed in the hope that it will be useful,but
  9. -- WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
  10. -- or  FITNESS FOR A PARTICULAR PURPOSE.   See the GNU General Public License 
  11. -- for  more  details.  You  should  have  received a copy of the GNU General 
  12. -- Public  License  along  with  SmallEiffel;  see the file COPYING.  If not,
  13. -- write to the  Free Software Foundation, Inc., 59 Temple Place - Suite 330,
  14. -- Boston, MA 02111-1307, USA.
  15. --
  16. class CLASS_INVARIANT
  17.    --
  18.    -- To store a `class invariant'.
  19.    --
  20.    
  21. inherit ASSERTION_LIST redefine pretty_print end;
  22.          
  23. creation make, make_runnable
  24.  
  25. feature 
  26.    
  27.    name: STRING is
  28.       do
  29.      Result := fz_invariant;
  30.       end;
  31.    
  32.    pretty_print is
  33.       local
  34.      i: INTEGER;
  35.       do
  36.      fmt.set_indent_level(0);
  37.      if not fmt.zen_mode then
  38.         fmt.skip(1);
  39.      end;
  40.      fmt.keyword(name);
  41.      if header_comment /= Void then
  42.         header_comment.pretty_print;
  43.      end;
  44.      if list /= Void then
  45.         from  
  46.            i := 1;
  47.         until
  48.            i > list.upper          
  49.         loop
  50.            fmt.set_indent_level(1);
  51.            fmt.indent;
  52.            if not fmt.zen_mode then
  53.           fmt.skip(1);
  54.            end;
  55.            fmt.set_semi_colon_flag(true);
  56.            list.item(i).pretty_print;
  57.            i := i + 1;
  58.         end;
  59.      end;
  60.       end;
  61.  
  62.    short(bc: BASE_CLASS) is
  63.       local
  64.      i: INTEGER;
  65.       do
  66.      bc.header_comment_for(Current);
  67.      short_print.hook_or("hook811","invariant%N");
  68.      if header_comment = Void then
  69.         short_print.hook_or("hook812","");
  70.      else
  71.         short_print.hook_or("hook813","");
  72.         header_comment.short("hook814","   -- ","hook815","%N");
  73.         short_print.hook_or("hook816","");
  74.      end;
  75.      if list = Void then
  76.         short_print.hook_or("hook817","");
  77.      else
  78.         short_print.hook_or("hook818","");
  79.         from  
  80.            i := 1;
  81.         until
  82.            i = list.upper          
  83.         loop
  84.            list.item(i).short("hook819","   ", -- before each assertion
  85.                   "hook820","", -- no tag
  86.                   "hook821","", -- before tag
  87.                   "hook822",": ", -- after tag
  88.                   "hook823","", -- no expression
  89.                   "hook824","", -- before expression
  90.                   "hook825",";", -- after expression except last
  91.                   "hook826","%N", -- no comment
  92.                   "hook827","", -- before comment
  93.                   "hook828"," -- ", -- comment begin line
  94.                   "hook829","%N", -- comment end of line
  95.                   "hook830","", -- after comment
  96.                   "hook831",""); -- end of each assertion
  97.  
  98.            i := i + 1;
  99.         end;
  100.         list.item(i).short("hook819","   ", -- before each assertion
  101.                    "hook820","", -- no tag
  102.                    "hook821","", -- before tag
  103.                    "hook822",": ", -- after tag
  104.                    "hook823","", -- no expression
  105.                    "hook824","", -- before expression
  106.                    "hook832",";", -- after last expression
  107.                    "hook826","%N", -- no comment
  108.                    "hook827","", -- before comment
  109.                    "hook828"," -- ", -- comment begin line
  110.                    "hook829","%N", -- comment end of line
  111.                    "hook830","", -- after comment
  112.                    "hook831","");
  113.         short_print.hook_or("hook833","");
  114.      end;
  115.      short_print.hook_or("hook834","");
  116.       ensure
  117.      fmt.indent_level = old fmt.indent_level;
  118.       end;
  119.  
  120. feature {NONE}
  121.    
  122.    check_assertion_mode: STRING is
  123.       do
  124.      Result := "inv";
  125.       end;
  126.       
  127. feature {RUN_CLASS}
  128.    
  129.    c_define is
  130.      -- Define C function to check invariant.
  131.       require
  132.      run_control.invariant_check;
  133.      current_type /= Void;
  134.      run_class.at_run_time;
  135.      small_eiffel.is_ready;
  136.      cpp.on_c
  137.       local
  138.      id: INTEGER;
  139.       do
  140.      id := current_type.id;
  141.      -- The invariant frame descriptor :
  142.      c_code.copy("se_frame_descriptor se_ifd");
  143.      id.append_in(c_code);
  144.      cpp.put_extern7(c_code);
  145.      c_code.copy("{%"Class invariant of ");
  146.      c_code.append(current_type.run_time_mark);
  147.      c_code.append("%",1,0,%"");
  148.      c_frame_descriptor_format.clear;
  149.      current_type.c_frame_descriptor;
  150.      c_code.append(c_frame_descriptor_format);
  151.      c_code.append("%",1};%N");
  152.      cpp.put_string(c_code);
  153.      -- The function :
  154.      c_code.clear;
  155.      c_code.extend('T');
  156.      id.append_in(c_code);
  157.      c_code.extend('*');
  158.      c_code.append(fz_se_i);
  159.      id.append_in(c_code);
  160.      c_code.append("(se_dump_stack*caller,T");
  161.      id.append_in(c_code);
  162.      c_code.append("*C)");
  163.      cpp.put_c_heading(c_code);
  164.      cpp.swap_on_c;
  165.      c_code.copy("se_dump_stack ds;%Nds.fd=&se_ifd");
  166.      id.append_in(c_code);
  167.      c_code.append(";%Nds.current=((void**)&C);%N");
  168.      cpp.put_string(c_code);
  169.      cpp.put_position_in_ds(start_position);
  170.      cpp.put_string(
  171.             "ds.caller=caller;%N%
  172.         %se_dst=&ds;%N");
  173.      compile_to_c;
  174.      cpp.put_string("se_dst=caller;%Nreturn C;%N}%N");
  175.       ensure     
  176.      cpp.on_c
  177.       end;
  178.    
  179. feature {NONE}   
  180.  
  181.    c_code: STRING is
  182.       once
  183.      !!Result.make(128);
  184.       end;
  185.  
  186. end -- CLASS_INVARIANT
  187.  
  188.